/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.subscope;

import java.util.HashSet;
import java.util.Iterator;
import java.util.Map;
import java.util.Set;
import java.util.TreeMap;
import java.util.TreeSet;

import alloy.ast.LeafId;
import alloy.ast.ModuleInfo;
import alloy.ast.QualifiedName;
import alloy.ast.SigExpr;
import alloy.ast.Signature;
import alloy.type.SigType;
import alloy.util.Dbg;

/**
 * Collects information on scoped sigs.
 * @see ScopedSigsInfo
 */
public class ScopedSigsInfoImpl implements ScopedSigsInfo {

    /**
       leaf ids of scoped sigs
    */
    private Set /* of LeafId */ _scopedSigIds = new TreeSet();

    /**
       map from leaf ids of scoped sigs to set of leaf ids of children
    */
    private Map /* from LeafId to Set of LeafId */ _sigId2ChildIds = new TreeMap();

    /**
       map from leaf ids of scoped sigs to leaf ids of parents
    */
    private Map /* from LeafId to LeafId */ _sigId2ParentId = new TreeMap();

    /**
       map from names of scoped sigs to leaf ids
    */
    private Map /* from String to LeafId */ _sigName2Id = new TreeMap();

    /**
       map from leaf ids of scoped sigs to names
    */
    private Map /* LeafId -> String */ _id2SigName = new TreeMap();
    
    private static final boolean DEBUG = false;

    /**
     * @param stringToType_ map from string signature names to their basic types
     */
    public ScopedSigsInfoImpl(Map stringToType_) {
        for (Iterator sigTypeIter = stringToType_.values().iterator();
             sigTypeIter.hasNext(); ) {
            // all signatures corresponding to basic types are scoped
            _handleScopedSig(((SigType)sigTypeIter.next()).getSignature());
        }
        // treat Int as a scoped sig
        // not 100% sure this is the right thing to do, esp. if Int does
        // not appear in model, but it should be fine
        //_scopedSigIds.add(IntType.INT_LEAF_ID);
        //_id2SigName.put(IntType.INT_LEAF_ID, "Int");
        //_sigName2Id.put("Int", IntType.INT_LEAF_ID);
        
    }

    /**
     * @param sig_ a scoped signature.  either a signature associated with a basic type,
     * or a disjoint signature extending exactly one scoped signature.  
     */
    private boolean _handleScopedSig(Signature sig_) {
        String sigName = sig_.getTypedName();
        if (DEBUG) System.err.println("handling scoped sig " + sigName);
        LeafId sigId = sig_.getLeafId();
        _scopedSigIds.add(sigId);
        _sigName2Id.put(sigName,sigId);
        _id2SigName.put(sigId,sigName);

	Set childIds = new HashSet();
        for (Iterator extBySigIter = sig_.getExtByIter(); extBySigIter.hasNext(); ) {
            Signature childSig = (Signature)extBySigIter.next();
            _sigId2ParentId.put(childSig.getLeafId(), sigId);
            childIds.add(childSig.getLeafId());
        }
        _sigId2ChildIds.put(sigId,childIds);

//         Set /* of LeafId */ disjChildIds = new TreeSet();
//         for (Iterator extBySigIter = sig_.getExtByIter();
//              extBySigIter.hasNext(); ) {
//             Signature childSig = (Signature)extBySigIter.next();
//             if (DEBUG) System.err.println("looking at extending sig " + childSig.getTypedName());

//             if (childSig.isDisj()) {
//                 // make sure sig doesn't already extend another disjoint sig
//                 LeafId childId = childSig.getLeafId();
//                 if (_sigId2ParentId.containsKey(childId)) {
//                     Dbg.user(new Msg("cannot extend two disjoint signatures",
//                                      childSig.getExtends()));
//                     return false;
//                 }
//                 if (!_handleScopedSig(childSig)) return false;
//                 if (DEBUG) System.err.println("disj sig " + childSig.getTypedName() + " extending " + sig_.getTypedName());
//                 _sigId2ParentId.put(childId, sigId);
//                 disjChildIds.add(childId);
//             }
//        }
        _sigId2ChildIds.put(sigId,childIds);
        return true;
    }
        
    private LeafId _getSigId(SigExpr sigExpr_,
                             ModuleInfo info_) {
        QualifiedName extSigName = sigExpr_.getSig();
        Signature extSig = info_.getSignature(extSigName, "");
        Dbg.chk(extSig);
        return extSig.getLeafId();
    }
        
    /**
     * @return <code>true</code> if id_ corresponds to a scoped sig; <code>false</code>
     * otherwise
     */
    public boolean isScopedSig(LeafId id_) {
        return _scopedSigIds.contains(id_);
    }

    /**
     * @return an {@link Iterator} over {@link LeafId leaf ids} of all the scoped
     * signatures which extend the scoped signature with leaf id id_
     */
    public Iterator /* over LeafId */ childSigIds(LeafId id_) {
        Dbg.chk(isScopedSig(id_));
        return ((Set)_sigId2ChildIds.get(id_)).iterator();
    }

    /**
     * @return the leaf id of the scoped signature which is the parent of the scoped
     * signature with leaf id id_, or <code>null</code> if there is no parent
     */
    public LeafId parentSigId(LeafId id_) {
        Dbg.chk(isScopedSig(id_));
        return (LeafId)_sigId2ParentId.get(id_);
    }
    
    /**
     * @return <code>true</code> if scoped signature with id child_ extends
     * <em>or</em> equals scoped signature with id ancestor_; <code>false</code>
     * otherwise
     */
    public boolean extendsOrEquals(LeafId child_, LeafId ancestor_) {
        Dbg.chk(isScopedSig(child_) && isScopedSig(ancestor_));
        if (child_.equals(ancestor_)) return true;
        LeafId parent = parentSigId(child_);
        if (parent == null) return false;
        return extendsOrEquals(parent, ancestor_);
    }

    /**
     * @return the leaf id for scoped signature with name sigName_, or <code>null</code>
     * if sigName_ does not correspond to a scoped signature
     */
    public LeafId getScopedSigId(String sigName_) {
        return (LeafId)_sigName2Id.get(sigName_);
    }
    
    /**
     * @return the name of the scoped signature with leaf id id_, or <code>null</code>
     * if no scoped signature has leaf id id_
     */
    public String getScopedSigName(LeafId id_) {
        return (String)_id2SigName.get(id_);
    }

}
